00010	VAR:x,y,z,u,s;
00020	INF_PRED:=;PRE_PRED:clear,on;
00030	PRE_OP: puton,A,B,C,T,S0,R;
00040	
00100	clear(x,s)∧clear(y,s)⊃on(x,y,R(puton(x,y),s));
00200	clear(x,s)⊃on(x,T,R(puton(x,T),s));
00300	clear(x,s) ≡ ∀y¬on(y,x,s);
00450	on(x,y,s)∧ ¬z=y ⊃clear(y,R(puton(x,z),s));
00500	
00600	clear(x,s)∧¬x=y ⊃ clear(x,R(puton(z,y),s));
00700	on(x,y,s)∧¬z=x ⊃ on(x,y,R(puton(z,u),s));
00800	clear(C,S0); clear(B,S0); 
00900	on(A,T,S0); on(B,T,S0); on(C,A,S0);
00950	¬A=B; ¬B=C; ¬C=A; ¬A=T;¬B=T; ¬C=T;
00975	-A=C; A=A; ¬B=A; B=B; ¬C=B; C=C;¬T=A;¬T=B;¬T=C;T=T;